home *** CD-ROM | disk | FTP | other *** search
/ Collection of Internet / Collection of Internet.iso / faq / comp / z_faq < prev   
Text File  |  1994-03-31  |  21KB  |  377 lines

  1. Newsgroups: comp.specification.z,news.answers,comp.answers
  2. Path: bloom-beacon.mit.edu!hookup!europa.eng.gtefsd.com!howland.reston.ans.net!pipex!uknet!comlab.ox.ac.uk!zforum-request
  3. From: zforum-request@comlab.ox.ac.uk
  4. Subject: comp.specification.z Frequently Asked Questions (Monthly)
  5. Message-ID: <z-faq_765162002@newsserv>
  6. Followup-To: comp.specification.z
  7. Summary: Information about the Z formal specification notation
  8. Originator: news@topaz.comlab
  9. Supersedes: <z-faq_762487202@newsserv>
  10. Sender: news@comlab.ox.ac.uk
  11. Reply-To: zforum-request@comlab.ox.ac.uk
  12. Organization: Oxford University Computing Laboratory, UK
  13. Date: Fri, 1 Apr 1994 01:00:04 GMT
  14. Approved: news-answers-request@MIT.Edu
  15. Expires: Fri, 13 May 1994 01:00:02 GMT
  16. Lines: 358
  17. Xref: bloom-beacon.mit.edu comp.specification.z:721 news.answers:17071 comp.answers:4366
  18.  
  19. Archive-name: z-faq
  20. Last-modified: 1 March 1994
  21.  
  22.  
  23. NAME:     comp.specification.z
  24. STATUS:   unmoderated
  25. PURPOSE:  Discussion concerning the formal specification notation Z.
  26.  
  27. (If you have read this before, changed and new sections since the
  28. previously issued version are marked with `|' in the right hand margin.)
  29.  
  30. Questions have been marked with "Subject:" at the start of the line to
  31. allow some newsreaders to scan them easily (e.g., "^G" within "rn").
  32.  
  33. Subject: What is it?
  34.  
  35. The comp.specification.z electronic USENET newsgroup was established in
  36. June 1991 and is intended to handle messages concerned with the formal
  37. specification notation Z (pronounced `zed'). It has an estimated
  38. readership of around 30,000 people worldwide.  Z, based on set theory
  39. and first order predicate logic, has been developed at the Programming
  40. Research Group (PRG) at the Oxford University Computing Laboratory and
  41. elsewhere for well over a decade.  It is now used by industry as part
  42. of the software (and hardware) development process in both the UK and
  43. the US. It is currently undergoing BSI standardization in the UK and
  44. has been accepted for the ISO standardization process internationally.
  45. Comp.specification.z provides a convenient forum for messages concerned
  46. with recent developments and the use of Z.  Pointers to and reviews of
  47. recent books and articles are particularly encouraged. These will be
  48. included in the Z bibliography (see below) if they appear in
  49. comp.specification.z.
  50.  
  51. Subject: What if I know someone interested without access to USENET news?
  52.  
  53. There is an associated Z FORUM electronic mailing list that was
  54. initiated in January 1986 by Ruaridh Macdonald, RSRE, UK.  Articles are
  55. now automatically cross-posted between comp.specification.z and the
  56. mailing list for those whose do not have access to USENET news.  This
  57. may apply especially to industrial Z users who are particularly
  58. encouraged to subscribe and post their experiences to the list.  Please
  59. contact <zforum-request@comlab.ox.ac.uk> with your name, address and
  60. email address to join the mailing list (or if you change your email
  61. address or wish to be removed from the list). Readers are strongly
  62. urged to read the comp.specification.z newsgroup rather than the Z
  63. FORUM mailing list if possible. Messages for submission to the Z FORUM
  64. mailing list and the comp.specification.z newsgroup may be emailed to
  65. <zforum@comlab.ox.ac.uk>.  This method of posting is particularly
  66. recommended for important messages like announcements of meetings since
  67. not all messages posted on comp.specification.z reach the PRG.
  68.  
  69. Subject: What if I know someone interested without access to email?
  70.  
  71. If you wish to join the postal Z mailing list, please send your address
  72. to Anthony Hall, Praxis Systems plc, 20 Manvers Street, Bath BA1 1PX,
  73. UK  (tel +44-225-444700, fax +44-225-465205, email <jah@praxis.co.uk>).
  74. This will ensure you receive details of Z meetings, etc., particularly
  75. for people without access to electronic mail.
  76.  
  77. Subject: How can I join in?
  78.  
  79. If you are currently using Z, you are welcome to introduce yourself to
  80. the newsgroup and Z FORUM list by describing your work with Z or
  81. raising any questions you might have about Z which are not answered
  82. here. You may also advertize publications concerning Z which you or
  83. your colleagues produce. These may then be added to the master Z
  84. bibliography maintained at the PRG.
  85.  
  86. Subject: Where are Z-related files archived?
  87.  
  88. There is an automatic electronic mail-based electronic archive server
  89. at the PRG which contains most messages and back-issues on
  90. comp.specification.z and Z FORUM, as well as a selection of other
  91. Z-related files.  Send an email message containing the command "help"
  92. to <archive-server@comlab.ox.ac.uk> for further information on how to
  93. use the server. A command of "index z" will list the Z-related files.
  94. If you have serious trouble accessing the archive server, please
  95. contact the address <archive-management@comlab.ox.ac.uk>.
  96.   The archive is also available via anonymous FTP on the Internet. Type
  97. the command "ftp ftp.comlab.ox.ac.uk" (or alternatively "ftp 163.1.27.2"
  98. if this does not work) and use "anonymous" as the login id and your
  99. email address as the password when prompted. The FTP command "cd pub/Zforum"
  100. will get you into the Z archive directory.  The file "README" gives
  101. some general information and "00index" gives a list of the files.
  102. (Retrieve these using the FTP command "get README", for example.)
  103.  
  104. Subject: What tools are available?
  105.  
  106. Various tools for formatting, type-checking and aiding proofs in Z are
  107. available.  A free LaTeX style file and documentation can be obtained
  108. from the PRG archive server. To receive this via email, send a message
  109. containing the command "send z zed.sty zguide.tex" to the PRG archive
  110. server (see above). A newer style "csp_zed.sty" is also available in
  111. the same location, which uses the new font selection scheme and covers
  112. CSP and Z symbols.
  113.   The fuzz package, a syntax and type checker with a LaTeX style option
  114. and fonts, is available from J.M. Spivey Computing Science Consultancy,
  115. 34, Westlands Grove, Stockton Lane, York YO2 0EF, UK. It is compatible
  116. with the second edition of Spivey's Z Reference Manual (see below).
  117. Contact Mike Spivey (email <Mike.Spivey@comlab.oxford.ac.uk>) for
  118. further information, or send the command "send z fuzz" to the PRG
  119. archive server for brief information and an order form.
  120.   CADiZ, a suite of tools for checking and typesetting Z specifications
  121. is available from York Software Engineering, University of York, York
  122. YO1 5DD, UK (tel +44-904-433741, fax +44-904-433744). Support is
  123. available for Unix troff and more recently for LaTeX. Further information
  124. is available from David Jordan at York on <yse@minster.york.ac.uk>.
  125.   ProofPower is a suite of tools supporting specification and proof in
  126. Higher-Order Logic (HOL) and in Z. Short courses on ProofPower-Z are
  127. available as demand arises.  Information about ProofPower can be
  128. obtained automatically from <ProofPower-server@win.icl.co.uk>.  Contact
  129. Roger Jones, International Computers Ltd, Eskdale Road, Winnersh,
  130. Wokingham, Berkshire RG11 5TT, UK (tel +44-734-693131 ext 6536, fax
  131. +44-734-697636, email <R.B.Jones@win0109.wins.icl.co.uk> or
  132. <rbj@win.icl.co.uk>) for further details.
  133.   Zola is a tool that supports the production and typesetting of Z
  134. specifications, including a type-checker and a Tactical Proof System.
  135. The tool is sold commercially and available to academic users at a
  136. special discount.  For further information, contact K. Ashoo, Imperial
  137. Software Technology, 62-74 Burleigh Street, Cambridge CB1 1DJ, UK (tel
  138. +44-223-462400, fax +44-223-462500, email <ka@ist.co.uk>).
  139.   ZTC is a Z type checker for the PC available free of charge via FTP
  140. from ise.cs.depaul.edu:/ftp/dist/ZTC1.2.tar.Z (140.192.32.117, login
  141. "ftp") and also from the Z archive at Oxford, together with a brief
  142. introduction in "ZTC". It is available for educational and non-profit
  143. uses and is part of an ongoing research project developing supporting
  144. tools for using Z. Contact Xiaoping Jia on <jia@cs.depaul.edu> for
  145. further information.
  146.   The B-Tool can be used to check proofs concerning parts of Z
  147. specifications.  This is licensed by Edinburgh Portable Compilers Ltd,
  148. 17 Alva Street, Edinburgh EH2 4PH, UK (tel +44-31-225-6262, fax
  149. +44-31-225-6644). Contact the Distribution Manager (email
  150. <support@epc.ed.ac.uk>) for further information.
  151.   The B-Toolkit is a set of integrated tools which fully supports the
  152. B-Method for formal software development and is available from B-Core
  153. (UK) Limited, Magdalen Centre, The Oxford Science Park, Oxford OX4 4GA,
  154. UK. For further details, contact Ib Sorensen (tel +44-865-784520,
  155. fax +44-865-784518, email <Ib.Sorensen@comlab.ox.ac.uk>).
  156.   Formaliser is a syntax-directed Z editor and type checker, running
  157. under Microsoft Windows, available from Logica Cambridge.  Contact
  158. Susan Stepney, Logica Cambridge Limited, Betjeman House, 104 Hills Road,
  159. Cambridge CB2 1LQ, UK  (tel +44-223-66343, email <susan@logcam.co.uk>)
  160. for further information.
  161.   A survey of Z tools may be obtained from Colin Parker, Systems Process
  162. Department, W376C, British Aerospace, Warton Aerodrome, Warton, Preston
  163. PR4 1AX, UK.
  164.  
  165. Subject: How can I learn about Z?
  166.  
  167. There are a number of courses on Z run by industry and academia. Oxford
  168. University offers industrial short courses in the use Z.  As well as
  169. introductory courses, recent newly developed material includes advanced
  170. Z-based courses on proof and refinement, partly based around the
  171. B-Tool.  Courses are held in Oxford, or elsewhere (e.g., on a company's
  172. premises) if there is enough demand. For further information, contact
  173. Jim Woodcock (tel +44-865-283514, fax +44-865-273839, email
  174. <Jim.Woodcock@comlab.ox.ac.uk>).
  175.   Logica Cambridge Limited offer a five day course on Z and a three day
  176. introductory course on formal methods (mainly Z).  For dates and prices
  177. contact Debi Kearney on +44-223-66343 ext 4859.
  178.   Praxis Systems plc runs a range of Z (and other formal methods) courses.
  179. For details contact Anthony Hall on +44-225-444700 or <jah@praxis.co.uk>.
  180.   Formal Systems (Europe) Ltd run a range of Z, CSP and other formal
  181. methods courses, primarily in the US and with such lecturers as Jim
  182. Woodcock and Bill Roscoe (both lecturers at the PRG).  For dates and prices
  183. contact Joy Reed (tel +44-865-283503, email <Joy.Reed@comlab.ox.ac.uk>)
  184. at the PRG or Kate Pearson (tel +44-865-728460) at Formal Systems.
  185.  
  186.  
  187. Subject: What has been published about Z?
  188.  
  189. A BibTeX bibliography of Z-related publications is available from the
  190. PRG archive server (see above).  Information on Oxford University
  191. Programming Research Group (PRG) Technical Monographs and Reports,
  192. including many on Z, is available from the librarian (tel +44-865-273837,
  193. fax +44-865-273839, email <library@comlab.ox.ac.uk>).
  194.   "Formal Methods: A Survey" by S.Austin & G.I.Parkin, March 1993
  195. includes information on the use and teaching of Z in industry and
  196. academia.  Contact DITC Office, Formal Methods Survey, National
  197. Laboratory, Teddington, Middlesex TW11 0LW, UK (tel +44-81-943-7002,
  198. fax +44-81-977-7091) for a copy.
  199.   The following books largely concerning Z have been or are due to be
  200. published (in approximate chronological order):
  201.  
  202.   I.Hayes (ed.), Specification case studies, Prentice Hall International
  203.       Series in Computer Science, 1987. (2nd ed., 1993)
  204.   J.M.Spivey, Understanding Z: a specification language and its formal
  205.       semantics, Cambridge University Press, 1988.
  206.   D.Ince, An introduction to discrete mathematics and formal system
  207.       specification, Oxford University Press, 1988. (2nd ed., 1992)
  208.   J.C.P.Woodcock & M.Loomes, Software engineering mathematics, Pitman, 1988.
  209.   J.M.Spivey, The Z notation: a reference manual, Prentice Hall
  210.       International Series in Computer Science, 1989. (2nd ed., 1992)
  211.       [Widely used as the current de facto standard for Z.]
  212.   A.Diller, Z: an introduction to formal methods, Wiley, 1990.
  213.   J.E.Nicholls (ed.), Z user workshop, Oxford 1989, Springer-Verlag,
  214.       Workshops in Computing, 1990.
  215.   B.Potter, J.Sinclair & D.Till, An introduction to formal specification
  216.       and Z, Prentice Hall International Series in Computer Science, 1991.
  217.   D.Lightfoot, Formal specification using Z, MacMillan, 1991.
  218.   A.Norcliffe & G.Slater, Mathematics for software construction,
  219.       Ellis Horwood, 1991.
  220.   J.E.Nicholls (ed.), Z user workshop, Oxford 1990, Springer-Verlag,
  221.       Workshops in Computing, 1991.
  222.   I.Craig, The formal specification of advanced AI architectures,
  223.       Ellis Horwood, 1991.
  224.   M.Imperato, An introduction to Z, Chartwell-Bratt, 1991.
  225.   J.B.Wordsworth, Software development with Z, Addison-Wesley, 1992.
  226.   S.Stepney, R.Barden & D.Cooper (eds.), Object orientation in Z,
  227.       Springer-Verlag, Workshops in Computing, August 1992.
  228.   J.E.Nicholls (ed.), Z user workshop, York 1991, Springer-Verlag,
  229.       Workshops in Computing, 1992.
  230.   D.Edmond, Information Modeling: Specification and Implementation,
  231.       Prentice Hall, 1992.
  232.   J.P.Bowen & J.E.Nicholls (eds.), Z user workshop, London 1992,
  233.       Springer-Verlag, Workshops in Computing, 1993.
  234.   S.Stepney, High integrity compilation: A case study, Prentice Hall, 1993.
  235.   M.McMorran & S.Powell, Z guide for beginners, Blackwell Scientific, 1993.
  236.   K.C.Lano & H.Haughton (eds.), Object-oriented specification case studies,
  237.       Prentice Hall International Object-Oriented Series, 1993.
  238. Announced:
  239.   B.Ratcliff, Introducing Specification Using Z: A Practical Case Study
  240.       Approach, McGraw-Hill, April 1994.
  241.   A.Diller, Z: an introduction to formal methods, 2nd ed., Wiley, c May 1994.
  242.       (In preparation)
  243.   J.P.Bowen & J.A.Hall (eds.), Z user workshop, Cambridge 1994,
  244.       Springer-Verlag, Workshops in Computing, June 1994.
  245.   J.C.P.Woodcock, Using standard Z, Prentice Hall International Series
  246.       in Computer Science, 1994? (In preparation)
  247.   R.Barden, S.Stepney, D.Cooper, Z in practice (A methods handbook for Z),
  248.       Prentice-Hall, 1994. (In preparation)
  249.  
  250. Subject: What is object-oriented Z?
  251.  
  252. Several object-oriented extensions to or versions of Z have been
  253. proposed.  The book "Object orientation in Z", listed above, is a
  254. collection of papers describing various OOZ approaches - Hall, ZERO,
  255. MooZ, Object-Z, OOZE, Schuman&Pitt, Z++, ZEST and Fresco (an OO VDM
  256. method) - in the main written by the methods' inventors, and all
  257. specifying the same two examples. A more recent book entitled
  258. "Object-oriented specification case studies" surveys the principal
  259. methods and languages for formal object-oriented specification,
  260. including Z-based approaches.
  261.  
  262. Subject: How can I run Z?
  263.  
  264. Z is a (non-executable in general) specification language, so there is
  265. no such thing as a Z compiler/linker/etc. as you would expect for a
  266. programming language. Some people have looked at animating subsets of Z
  267. for rapid prototyping purposes, using logic and functional programming
  268. for example, but this work is preliminary and is not really the major
  269. point of Z, which is to increase human understandability of the
  270. specified system and allow the possibility of formal reasoning and
  271. development. However, Prolog seems to be the main favoured language for
  272. Z prototyping and some references may be found in the Z bibliography
  273. (see above).
  274.  
  275. Subject: Where can I meet other Z people?
  276.  
  277. The 7th annual Z User Meeting with an industrial theme was held on
  278. 14-15 December 1992 at the DTI A preprint proceedings and draft Z
  279. standard were distributed to delegates. A published proceedings is in
  280. press; ordering details are available from the Z archive (see above) in
  281. the file "zum92". An 8th meeting (ZUM'94) is planned for 29-30 June
  282. 1994 at St. John's College, University of Cambridge, UK in association
  283. with BCS FACS. A Call for Participation is available in the Z archive
  284. (see above) in the file "zum94". For general enquiries, contact the
  285. Conference Chair, Jonathan Bowen (tel +44-865-283512, fax +44-865-273839,
  286. email <Jonathan.Bowen@comlab.ox.ac.uk>).
  287.   The 6th Refinement Workshop was held at City University, London, UK,
  288. 5-7 January 1994. The Programme Chair was David Till, Dept of Computer
  289. Science, City University, Northampton Square, London, EC1V 0HB, UK (tel
  290. +44-71-477-8552, email <till@cs.city.ac.uk>).  The proceedings for these
  291. workshops are currently published in the Springer-Verlag Workshops in
  292. Computing series.
  293.   The first FME (Formal Methods Europe) Symposium was held in Odense,
  294. Denmark, 19-23 April 1993.  The proceedings are available as Springer
  295. LNCS 670. The next FME Symposium will be held 24-28 October 1994 in
  296. Barcelona, Spain.  The Programme Chair is Tim Denvir (tel +44-81-882-5853,
  297. fax +44-81-8823118, email <timdenvir@cix.compulink.co.uk>) and the
  298. Organizing Chair in Spain is Daniel Cabedo (tel +34-3-290-2400, fax
  299. +34-3-290-2416, email <felixrp@salleserver.url.es>). The chairman of
  300. FME is Martyn Thomas, Praxis plc, 20 Manvers Street, Bath BA1 1PX, UK
  301. (tel +44-225-444700, email <mct@praxis.co.uk>).
  302.   FORTE addresses formal techniques and testing methodologies
  303. applicable to distributed systems such as Estelle, Lotos, SDL, ASN.1,
  304. Z, etc.  FORTE'93 was held at Boston, Massachusetts, USA on 26-29
  305. October 1993.  The IFIP WG6.1 7th International Conference on Formal
  306. Description Techniques for Distributed Systems and Communications
  307. Protocols will be held at Berne, Switzerland, 4-7 October 1994.  For
  308. further information contact:  FORTE'94 Organization Committee,
  309. University of Berne, PO Box 900, CH-3000 Bern 9, Switzerland (tel
  310. +41-31-631-4994 (Dieter Hogrefe), -4430 (Stefan Leue), fax -3965, email
  311. <forte94@iam.unibe.ch>). Additional information is available via anonymous
  312. FTP from the host "siam.unibe.ch" under the directory "forte94" (see the
  313. file "README" first).
  314.   Details of Z-related meetings may be advertized on comp.specification.z
  315. if desired. All the above meetings are likely to be repeated in some form.
  316.  
  317. Subject: What is the Z User Group?
  318.  
  319. The Z User Group was set up in 1992 to oversee Z-related activities, and
  320. the Z User Meetings in particular.  As a subscriber to comp.specification.z,
  321. ZFORUM or the postal mailing list, you may consider yourself a member
  322. of the Z User Group.  There are currently no charges for membership,
  323. although this is subject to review if necessary.  Contact
  324. <zforum-request@comlab.ox.ac.uk> for further information.
  325.  
  326. Subject: How can I obtain the draft Z standard?
  327.  
  328. The proposed Z standard under ISO/IEC JTC1/SC22 is available
  329. electronically via anonymous FTP *only* (not via the mail server since
  330. it is too large) from the Z archive at Oxford in PostScript format.
  331. Version 1.0 of the draft standard is accessible as "zstandard1.0.ps"
  332. together with the appendices in "zstandard-annex1.0.ps".  It is also
  333. available in printed form from the Oxford University Computing
  334. Laboratory librarian (tel +44-865-273837, fax +44-865-273839, email
  335. <library@comlab.ox.ac.uk>) by requesting Technical Monograph number
  336. PRG-107.
  337.  
  338. Subject: Where else is Z discussed?
  339.  
  340. The BCS FACS (British Computer Society Formal Aspects of Computer
  341. Science special interest group) and FME (Formal Methods Europe) are two
  342. organizations interested in formal methods in general. Contact BCS
  343. FACS, Dept of Computer Studies, Loughborough University of Technology,
  344. Loughborough, Leicester LE11 3TU, UK (tel +44-509-222676, fax
  345. +44-509-211586, email <FACS@lut.ac.uk>) for further information. A
  346. "FACS Europe" newsletter is issued to members of FACS and FME.  Please
  347. send suitable Z-related material to the Z column editor, David Till,
  348. Dept of Computer Science, City University, Northampton Square, London,
  349. EC1V 0HB, UK (tel +44-71-477-8552, email <till@cs.city.ac.uk>) for
  350. possible publication.  Material from articles appearing on the
  351. comp.specification.z newsgroup may be included if considered of
  352. sufficient interest (with permission from the originator if possible).
  353. It would be helpful for posters of articles on comp.specification.z to
  354. indicate if they do not want further distribution for any reason.
  355.  
  356. Subject: How does VDM compare with Z?
  357.  
  358. See I.J.Hayes, C.B.Jones & J.E.Nicholls, Understanding the differences
  359. between VDM and Z, FACS Europe, series I, 1(1):7-30, Autumn 1993 and
  360. I.J.Hayes, VDM and Z: A comparative case study, Formal Aspects of
  361. Computing, 4(1):76-99, 1992. VDM is discussed on the (unmoderated)
  362. VDM FORUM mailing list. Send a message containing the command
  363. "join vdm-forum <name>" where <name> is your real name to
  364. <mailbase@mailbase.ac.uk>. To contact the list administrator, email
  365. John Fitzgerald at the University of Newcastle upon Tyne, England, on
  366. <vdm-forum-request@mailbase.ac.uk>.
  367.  
  368. Subject: What if I have spotted a mistake or an omission?
  369.  
  370. Please send corrections or new relevant information about meetings,
  371. books, tools, etc., to <zforum-request@comlab.ox.ac.uk>.  New questions
  372. and model answers are also gratefully received!
  373.  
  374. --
  375. Jonathan Bowen, <Jonathan.Bowen@comlab.ox.ac.uk>
  376. Programming Research Group, Oxford University Computing Laboratory, UK.
  377.